1. Field of the Invention
The invention relates in general to assertion based verification and in particular to a system for analyzing the output of a circuit simulator to determine whether a circuit design possesses assertion properties, and whether it violates or fulfills the assertion properties, and for generating a display helping a user trace sources of the assertion property violations and fulfillments.
2. Description of Related Art
A circuit designer initially employs a hardware description language (HDL) such as Verilog to describe the behavior of an integrated circuit or a portion of an IC, using HDL statements to define logical relationships between signals. The designer then uses a computer-aided synthesis tool to create a gate level circuit design describing the circuit as a set of interconnected instances of standard circuit components (“standard cells”) such as transistors, logic gates and memories. After producing the gate level description, the designer uses computer-aided placement and routing tools to generate an integrated circuit (IC) layout design, providing a guide for IC fabrication by indicating the structure, position and orientation of each cell within the IC and indicating the routes signal paths follow between the cell terminals. The HDL description is further updated to include models of the temporal behavior signal paths interconnecting cell terminals.
To determine whether the circuit described by an HDL file at any stage of the design process will behave as expected, a designer can program a circuit simulator to simulate its response to a set of input signals. A simulator program (a “testbench”) includes the HDL description of the circuit, specifies the time-varying behavior of the circuit's input signals, indicates which of the circuit's input, internal and output signals are to be monitored during the simulation, and specifies various other parameters of the simulation. As it simulates the circuit, the simulator produces a “dump file” indicating the behavior of the monitored signals over time. The designer can use debugging tools to study the circuit behavior represented by the dump file to determine whether the circuit will behave as expected.
As circuits grow larger and more complex, it has become increasingly difficult and time consuming to fully test and debug circuit designs using simulation alone. In recent years, designers have begun supplementing simulation with “assertion based verification”. Assertions describe certain properties of a circuit that are expected to hold true. For example, an assertion may indicate that a property of the output data of an adder should always match the sum of its input data values within some specified time range after the adder is clocked. Assertion based verification tools external to a simulator can evaluate such assertions based on the signal data included in the dump file, provided that the dump file contains all signal data needed to evaluate the assertion.
A designer may incorporate “assertion statements” into the HDL description of a circuit executed by a simulator which do not affect the nature of the circuit described by the HDL design, but which tell the simulator to determine whether the circuit exhibits various properties the assertion statements describe and to report any instance in which a property fails to hold true. Thus even when the simulator is not programmed to include signal data need to evaluate an assertion among the data describing “observable” signals normally recorded in the dump file, the simulator can nonetheless monitor those signals and report any property violation including values of any signals needed to evaluate the property at the time of the violation. U.S. Patent Application Publication 2006/0085774 filed Oct. 14, 2004 teaches an assertion report produced by a simulator.
Generally, there are two kinds of assertions. Concurrent (also called “declarative”) assertions state that a given property must always be true throughout a simulation, while immediate assertions apply only for a limited time, or under specified conditions. The following example illustrates a typical syntax of a declarative assertion statement. The assert statement specifies that the property, test_adder, should yield FALSE if it is violated, or yield TRUE if it is fulfilled.
assert property (test_adder);
A testable property, such as test_adder, within an assertion may be a function of one or more signal values at specific times s can be a simple Boolean expression such as, for example,
property p0;  @(posedge clk)  t1 + t2 >= 1;end propertyThis expression indicates that the sum of values represented by signals t1 and t2 should be greater than or equal to 1 on the positive edge of the CLK signal. A property can also be in the form of a “sequence” of expressions to be evaluated in increasing order of time, such as for example,
property p1;  @(posedge clk)  ((((t1+t2) >= 1)  ##1:3 ((t1+bus2) >= (bus1 − t2) +2)))  ##2 ((bus1 +(t1 && !t2)) <=bus2))  ##1:3 (s1 or s2);end propertyThe above property indicates the following:
1. On the positive edge of a clock signal clk: the expression t1+t2>=1 should be TRUE.
2. On one of the next three clk signal edges, the expression (t1+bus2)>=(bus1−t2)+2) should become TRUE,
3. Two clock cycles later, the expression (bus1+(t1 && !t2))<=bus2 should be TRUE.
4. On one of the next three clk signal edges, the expression (s1 or s2) should become TRUE.
The p1 property will be FALSE if any one of its five expressions are FALSE and will be TRUE only if each of the five expressions is TRUE. Note that the simulator will require many clock cycles to evaluate the full expression.
Thus the assertion not only defines a property using a sequence of expressions, but it also defines an evaluation time corresponding to each expression, wherein the “evaluation time” is a simulation time at which the expression evaluates true or false. For example the property p1 term##1:3((t1+bus2)>=(bus1−t2)+2)))means that the evaluation time for expression ((t1+bus2)>=(bus1−t2)+2) should be either on the first, second or third clock signal clk edge following the evaluation time of the preceding expression (t1+t2)>=1. If the expression ((t1+bus2)>=(bus1−t2)+2) evaluates true on any of those three clock edges, then its “evaluation time” is the simulation time corresponding to the first one of those three clock signal edges. If the expression ((t1+bus2)>=(bus1−t2)+2) fails to evaluate true on any of those three clock edges, then its “evaluation time” is the simulation time corresponding to the last one of those three clock signal edges. The code “#1:3” thus defines the evaluation time of the expression.
One sequence may be nested within another. For example in the above expressions s1 and s2 are names of separately defined sequences. For example sequence s1 may be defined by the following code:
sequence s1;  ((t1 == 1) ##3 ((bus1 >2) && (t2 == 1));end sequenceThus a circuit property is expressed as a sequence of one or more expressions, each of which is a function of one or more variables, such as t1, bus1 or s1, each representing the value of either a signal, a group of signals or of another sequence. Each expression of a property is evaluated at a corresponding evaluation time defined by the assertion.
An assertion statement causes a simulator to report when a simulated circuit fails to exhibit the property and to report the states of the signals that affect the property evaluation. By providing targets for formal verification, assertions improve controllability by improving test coverage and observability, however although a designer can determine from an assertion message that a circuit design failed to exhibit a particular property at a particular time during the simulation, the message does not directly indicate where the source of the error lies in the circuit design. To determine that, the designer needs to analyze both the assertion statement and the circuit design to trace the error back to its source. What is needed is a system for helping the designer does that.